The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
The well-known completeness theorem of Bergstra & Tucker [BT82,BT97] states that all computable data types can be specified without quantifiers, i.e., quantifiers can be dispensed with–at least if the introduction of auxiliary (hidden) functions is allowed. However, the situation concerning the specification without hidden functions is quite different. Our main result is that, in this case,...
We consider in this paper an extension of Datalog with mechanisms for temporal, nonmonotonic and nondeterministic reasoning, which we refer to as Datalog++. We study its semantics, and show how iterated fixpoint and stable model semantics can be combined to the purpose of clarifying the interpretation of Datalog++ programs, and supporting their efficient execution. On this basis, the design of appropriate...
We study revision programming, a logic-based mechanism for enforcing constraints on databases. The central concept of this approach is that of a justified revision based on a revision program. We show that for any program P and for any pair of initial databases I and I’ we can transform (shift) the program P to a program P’ so that the size of the resulting program does not increase and so that P-justified...
In this paper, we consider the free-variable variant of the calculus KE and investigate the effect of different preprocessing activities to the proof length of variants of KE. In this context, skolemization is identified to be harmful as compared to the δ-rule. This does not only have consequences for proof length in KE, but also for the “efficiency” of some structural translations. Additionally,...
A choice construct can be added to fixpoint logic to give a more expressive logic, as shown in [GH]. On the other hand, a more straightforward way of increasing the expressive power of fixpoint logic is to add generalized quantifiers, corresponding to undefinable properties, in the sense of Lindström. The paper studies the expressive power of the choice construct proposed in [GH] in its relationships...
In our paper, we prove that Graph Connectivity is not in Monadic NP even in the presence of a built-in relation of arbitrary degree that does not have for an arbitrary, but fixed k ≥ 2 ∈ IN the complete graph Kk as a minor. We obtain our result by using the method of indiscernibles and giving a winning strategy for the duplicator in the Ajtai-Fagin Ehrenfeucht-Fraïssé Game...
We look at various uniform and non-uniform complexity classes within P/poly and its variations L/poly, NL/poly, NP/poly and PSpace/poly, and look for analogues of the Ajtai-Immerman theorem which characterizes AC0 as the non-uniformly First Order Definable classes of finite structures. We have previously observed that the Ajtai-Immerman theorem can be rephrased in terms of invariant definability...
We show that deciding the winner of the r-moves Ehrenfeucht-Fraïssé game on two finite structures A and B, over any fixed signature Σ that contains at least one binary and one ternary relation, is PSPACE complete. We consider two natural modifications of the EF game, the one-sided r-moves EF game, where the spoiler can choose from the first structure A only, and therefore the duplicator wins only...
We consider upper bounds for minimal resolution refutations of propositional formulas in CNF. We show that minimal refutations of minimal unsatisfiable formulas over n variables and n+k clauses consist of at most 2k − 1n2 applications of the resolution rule.
J. Krajíc̆ek and P. Pudlák proved that an almost optimal deterministic algorithm for TAUT exists if and only if there exists a p-optimal proof system for TAUT. In this paper we prove that an almost optimal deterministic algorithm for SAT exists if and only if there exists a p-optimal proof system for SAT. Combining Krajícek and Pudlák’s result with our result we show that an optimal deterministic...
Characteristic properties of majorant-computable real-valued functions are studied. A formal theory of computability over the reals which satisfies the requirements of numerical analysis used in Computer Science is constructed on the base of the definition of majorant-computability proposed in [13]. A model-theoretical characterization of majorant-computability real-valued functions and their domains...
This paper describes principles behind a declarative programming language CL (Clausal Language) which comes with its own proof system for proving properties of defined functions and predicates. We use our own implementation of CL in three courses in the first and second years of undergraduate study. By unifying the domain of LISP’s S-expressions with the domain ℕ of natural numbers we have combined...
The first philosophically motivated sentential logics to be proved undecidable were relevant logics like R and E. But we deal here with important decidable fragments thereof, like . Their decidability rests on S. Kripke’s gentzenizations, together with his central combinatorial lemma. Kripke’s lemma has a long history and was reinvented several times. It turns out equivalent...
Pure Type Systems ( PTS βs) provide a parametric framework for typed λ-calculi à la Church [1,2,10,11]. One important aspect of PTS βs is to feature a definitional equality based on β-conversion. In some instances however, one desires a stronger definitional equality based on βη-conversion. The need for such a strengthened definitional equality arises...
We define a class of hyperbalancedλ-terms by imposing syntactic constraints on the construction of λ-terms, and show that such terms are strongly normalizable. Furthermore, we show that for any hyperbalanced term, the total number of superdevelopments needed to compute its normal form can be statically determined at the beginning of reduction. To obtain the latter result, we develop an algorithm that,...
Solving systems of subtype constraints (or subtype inequalities) is in the core of efficient type reconstruction in modern object-oriented languages with subtyping and inheritance, two problems known polynomial time equivalent. It is important to know how different combinations of type constructors influence the complexity of the problem. We show the NP-hardness of the satisfiability problem...
Several systems of fixed-point types (also called retract types or recursive types with explicit isomorphisms) extending system F are considered. The seemingly strongest systems have monotonicity witnesses and use them in the definition of beta reduction for those types. A more naïve approach leads to non-normalizing terms. All the other systems are strongly normalizing because they embed in a reduction-preserving...
The set theoretic connection between functions and partitions is not worthy of further remark. Nevertheless, this connection turns out to have deep consequences for the theory of the Ershov numbering of lambda terms and thus for the connection between lambda calculus and classical recursion theory. Under the traditional understanding of lambda terms as function definitions, there are morphisms of...
We place simple axioms on an elementary topos which suffice for it to provide a denotational model of call-by-value PCF with sum and product types. The model is synthetic in the sense that types are interpreted by their set-theoretic counterparts within the topos. The main result characterises when the model is computationally adequate with respect to the operational semantics of the programming language...
We investigate a λ calculus with positive inductive and coinductive types , which we call λμ,ν, using logical relations. We show that parametric theories have the strong categorical properties, that the representable functors and natural transformations have the expected properties. Finally we apply the theory to show that terms of functorial type are almost canonical...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.